/***********************************************************************************************************************
*                                                                                                                      *
* SPLASH build system v0.1                                                                                             *
*                                                                                                                      *
* Copyright (c) 2013 Andrew D. Zonenberg                                                                               *
* All rights reserved.                                                                                                 *
*                                                                                                                      *
* Redistribution and use in source and binary forms, with or without modification, are permitted provided that the     *
* following conditions are met:                                                                                        *
*                                                                                                                      *
*    * Redistributions of source code must retain the above copyright notice, this list of conditions, and the         *
*      following disclaimer.                                                                                           *
*                                                                                                                      *
*    * Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the       *
*      following disclaimer in the documentation and/or other materials provided with the distribution.                *
*                                                                                                                      *
*    * Neither the name of the author nor the names of any contributors may be used to endorse or promote products     *
*      derived from this software without specific prior written permission.                                           *
*                                                                                                                      *
* THIS SOFTWARE IS PROVIDED BY THE AUTHORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED   *
* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL *
* THE AUTHORS BE HELD LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES        *
* (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR       *
* BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT *
* (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE       *
* POSSIBILITY OF SUCH DAMAGE.                                                                                          *
*                                                                                                                      *
***********************************************************************************************************************/

#include "splashcore.h"

using namespace std;

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// Construction / destruction

YosysProofUnitTestNode::YosysProofUnitTestNode(
	BuildGraph* graph,
	RTLILNetlistNode* netlist,
	string name,
	string partition)
	: UnitTestNode(graph, "", name, partition)
	, m_netlist(netlist)
	, m_timelimit(300)
	, m_maxIters(0)
{
}

YosysProofUnitTestNode::~YosysProofUnitTestNode()
{
	
}

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// Testing

string YosysProofUnitTestNode::GetHash()
{
	DebugPrintfHeading(4, "YosysProofUnitTestNode::GetHash()\n");
	string hashin = "";
	
	//Update our dependencies
	UpdateDependencies();
	
	//Add data at this node
	hashin += sha256(m_name);
	
	//Add data for our dependencies
	for(size_t i=0; i<m_dependencies.size(); i++)
		hashin += m_dependencies[i]->GetHashCached(); 
		
	//Add data for our preconditions
	for(auto x : m_preconditions)
		hashin += sha256(x.first) + sha256(x.second);
		
	return sha256(hashin);
}

void YosysProofUnitTestNode::UpdateDependencies()
{
	DebugPrintfHeading(4, "YosysProofUnitTestNode::UpdateDependencies() [name = %s]\n", m_name.c_str());
	
	UnitTestNode::UpdateDependencies();
	
	if(m_netlist != NULL)
		m_dependencies.push_back(m_netlist);
}

void YosysProofUnitTestNode::AddPrecondition(string sig1, string sig2)
{
	m_preconditions.push_back(pair<string, string>(sig1, sig2));
}

void YosysProofUnitTestNode::Update(Cluster* cluster)
{
	DebugPrintfSilent(5, "    Re-test is necessary\n");
	
	//Rebuild our dependencies (in case any source files were auto-generated, etc)
	vector<ClusterJob*> deps;
	for(size_t i=0; i<m_dependencies.size(); i++)
	{
		BuildGraphNode* node = m_dependencies[i];
		node->UpdateCached(cluster);
		if(node->GetBuildJob() != NULL)
			deps.push_back(node->GetBuildJob());
	}
	
	//Run the test
	m_job = m_netlist->GetToolchain()->ProveAssertions(
		m_netlist->GetOutputPath(),
		m_name,
		m_graph->GetMetaDir() + "/" + GetHashCached(),
		m_maxIters,
		m_preconditions,
		m_shows,
		deps,
		cluster);
}

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// Factory method

YosysProofUnitTestNode* YosysProofUnitTestNode::CreateYosysProofUnitTestNode(
	BuildGraph* graph,
	RTLILNetlistNode* netlist,
	string name,
	string partition)
{
	YosysProofUnitTestNode* node = new YosysProofUnitTestNode(
		graph, netlist, name, partition);
	graph->AddNode(node);
	graph->AddTest(node);
	return node;
}
